A:Type, eq:EqDecider(A), f, g:a:A fp Top, L:(A List).
l_disjoint(A;f  g.1;L)  (l_disjoint(A;f.1;L) & l_disjoint(A;g.1;L)) 

latex

Definitions	P  Q, t.1, t  T, P  Q, x:A. B(x), l_disjoint(T;l1;l2), , P & Q, Top, P  Q, x. t(x), EqDecider(T), a:A fp B(a), f  g, x  dom(f), b, P  Q, (x  l), False, A, {T}
Lemmas	pi1 wf, l member wf, fpf-join-dom, assert wf, fpf-dom wf, fpf wf, deq wf, l disjoint-fpf-dom, fpf-join wf, top wf, l disjoint wf